/*@
*/
int main()
{
 int i;
 i=0;
 while(i<10) /*@ */
 {
  print(i);
  i=i+1;
 }
 return 0;
}
/*@ i==10
*/
